$\forall$$A$, $B$:Type. ($\forall$$x$, $y$:$A$. Dec($x$ $=$ $y$)) $\Rightarrow$ ($\forall$$u$, $v$:$B$. Dec($u$ $=$ $v$)) $\Rightarrow$ ($\forall$$x$, $y$:$A$+$B$. Dec($x$ $=$ $y$))